|
In programming language semantics, normalisation by evaluation (NBE) is a style of obtaining the normal form of terms in the λ calculus by appealing to their denotational semantics. A term is first ''interpreted'' into a denotational model of the λ-term structure, and then a canonical (β-normal and η-long) representative is extracted by ''reifying'' the denotation. Such an essentially semantic approach differs from the more traditional syntactic description of normalisation as a reductions in a term rewrite system where β-reductions are allowed deep inside λ-terms. NBE was first described for the simply typed lambda calculus. It has since been extended both to weaker type systems such as the untyped lambda calculus using a domain theoretic approach, and to richer type systems such as several variants of Martin-Löf type theory. == Outline == Consider the simply typed lambda calculus, where types τ can be basic types (α), function types (→), or products (×), given by the following Backus–Naur Form grammar (→ associating to the right, as usual): :(Types) τ ::= α | τ1 → τ2 | τ1 × τ2 These can be implemented as a datatype in the meta-language; for example, for Standard ML, we might use:
Terms are defined at two levels. The lower ''syntactic'' level (sometimes called the ''dynamic'' level) is the representation that one intends to normalise. :(Syntax Terms) ''s'',''t'',… ::= var ''x'' | lam (''x'', ''t'') | app (''s'', ''t'') | pair (''s'', ''t'') | fst ''t'' | snd ''t'' Here lam/app (resp. pair/fst,snd) are the intro/elim forms for → (resp. ×), and ''x'' are variables. These terms are intended to be implemented as a first-order in the meta-language:
The denotational semantics of (closed) terms in the meta-language interprets the constructs of the syntax in terms of features of the meta-language; thus, lam is interpreted as abstraction, app as application, etc. The semantic objects constructed are as follows: :(Semantic Terms) ''S'',''T'',… ::= LAM (λ''x''. ''S'' ''x'') | PAIR (''S'', ''T'') | SYN ''t'' Note that there are no variables or elimination forms in the semantics; they are represented simply as syntax. These semantic objects are represented by the following datatype:
There are a pair of type-indexed functions that move back and forth between the syntactic and semantic layer. The first function, usually written ↑τ, ''reflects'' the term syntax into the semantics, while the second ''reifies'' the semantics as a syntactic term (written as ↓τ). Their definitions are mutually recursive as follows: These definitions are easily implemented in the meta-language:
By induction on the structure of types, it follows that if the semantic object ''S'' denotes a well-typed term ''s'' of type τ, then reifying the object (i.e., ↓τ S) produces the β-normal η-long form of ''s''. All that remains is, therefore, to construct the initial semantic interpretation ''S'' from a syntactic term ''s''. This operation, written ∥''s''∥Γ, where Γ is a context of bindings, proceeds by induction solely on the term structure: In the implementation:
Note that there are many non-exhaustive cases; however, if applied to a ''closed'' well-typed term, none of these missing cases are ever encountered. The NBE operation on closed terms is then:
As an example of its use, consider the syntactic term SKK defined below:
This is the well-known encoding of the identity function in combinatory logic. Normalising it at an identity type produces:
The result is actually in η-long form, as can be easily seen by normalizing it at a different identity type:
抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Normalisation by evaluation」の詳細全文を読む スポンサード リンク
|